M1, M2:MsgA. M1  M2  (k:Knd, x:Id. M2.rframe(k reads x)  M1.rframe(k reads x)) 

latex

Definitions	M.rframe(k reads x), M1  M2, MsgA, Valtype(da;k), P & Q, z != f(x)  P(a;z), x  dom(f), IdDeq, a:A fp B(a), Top, x. t(x), x.A(x), IdLnk, x:AB(x), b, , Prop, deq-member(eq;x;L), EqDecider(T), Type, T, KindDeq, s = t, <a,b>, f(x), type List, Knd, Id, True, f  g, x:A. B(x), P  Q, t  T, A & B, x:AB(x)
Lemmas	Kind-deq wf, Knd wf, deq wf, true wf, squash wf, deq-member wf, bool wf, assert wf, Id wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, msga wf, ma-sub wf, ma-rframe wf